{-# LANGUAGE KindSignatures             #-}
{-# OPTIONS -Wall #-}

--------------------------------------------------------------------------------
-- |
-- Module      :  ConfigCheck.Checker
-- Copyright   :  (c) Stephen Tetley 2014
-- License     :  BSD3
--
-- Maintainer  :  stephen.tetley@gmail.com
-- Stability   :  unstable
-- Portability :  GHC
--
-- Checker monad.
-- 
--------------------------------------------------------------------------------

module ConfigCheck.Checker
  (

    CheckError
  , ErrorMessage
  , Result
  , CheckerGroup(..)
  , Checker(..)
  , CheckFun
  , CheckCode
  , runChecker
  , runCheckers
  , runGroups
  , annotate
  , censor
  , failure
  , throwError
  , substError
  , swapPrimError
  , (<??>) 
  , (<&&>)
  , (<||>)

  , focus
  , self
  , (<<<)       -- Re-export from Control.Category
  , (>>>)       -- Re-export from Control.Category

  , selftest
  , selftest_
  , ask
  , asks
  , get
  , assert
  , assert_
  , assert1
  , assert1_
  , assert2
  , assert2_

  , whenTrue
  , unlessTrue
  , whenOK
  , unlessOK

  , whenJust
  , onlyJust

  , whenLeft
  , whenRight
  , onlyLeft
  , onlyRight

  , checkall
  , checkany
  , checkfirst
  , checklast

  , indexed
  , Indexed(..)
  , ZeroIxList
  , zeroIndexedList
  , OneIxList
  , oneIndexedList

  , countingChecker
  , exactly
  , atmost
  , atleast
  , withinCount

  -- Error messages
  , errMsg0
  , errMsg1
  , errMsg2
  , errMsg3
  , errMsg4
  , errMsg5

  -- Abstract report
  , GetName(..)
  , Priority(..)
  , CheckReport(..)
  , IssueGroup(..)
  , printReportSimple

  ) where

import Control.Applicative
import Control.Category ( (>>>), (<<<) )
import Control.Monad

import Text.PrettyPrint.HughesPJ hiding ( (<>) )
import qualified Text.PrettyPrint.HughesPJ as P

-- Base Imports
import Data.Either
import qualified Data.Foldable          as F
import qualified Data.IntMap            as IM
import Data.Maybe ( catMaybes ) 
import Data.Monoid
import Text.Printf

import Prelude hiding ( pred )


--------------------------------------------------------------------------------
-- Utility - Hughes lists (aka DList)

type H a = [a] -> [a]


unH :: H a -> [a]
unH = ($ [])

emptyH :: H a 
emptyH = id

wrapH :: a -> H a
wrapH a = (a:)

-- appendH :: H a -> H a -> H a
-- appendH = (.)

-- consH :: a -> H a -> H a
-- consH a = ((a:) .) 


--------------------------------------------------------------------------------



data CheckError p = CheckError !p !String [String]
  deriving (Eq,Show)

type ErrorMessage = String

-- AbstractReport data type?



--
-- DESIGN NOTE
--
-- It would be simpler to have `Okay ()` as success and thus 
-- `Fail msg` would be the only notion of failure. 
--
-- However, having two failure signals (Fail and `Okay False`) 
-- lets us write Applicative Checkers:
-- 
-- e.g. span < empty distance
--
-- > code = focus sensor $
-- >            (<) <$> get sensor_span <*> get sensor_empty_distance
--
--

data CheckerGroup p o = CheckerGroup
    { group_name                :: String 
    , group_checker_specs       :: [Checker p o]
    }

data Checker p o = Checker
    { checker_name              :: String
    , checker_description       :: String
    , checker_priority          :: p
    , checker_code              :: CheckFun o
    }

type CheckFun o = CheckCode o Result



data Result = OK 
            | UserFail ErrorMessage
            | PrimFail ErrorMessage 

-- | Concatenation is boolean-AND, modulo noise due to error 
-- messages.
--
instance Monoid Result where
  mempty                            = OK
  OK         `mappend` OK           = OK
  UserFail a `mappend` UserFail b   = UserFail $ unwords [a,b]
  UserFail a `mappend` _            = UserFail a
  _          `mappend` UserFail b   = UserFail b
  PrimFail a `mappend` _            = PrimFail a
  _          `mappend` PrimFail b   = PrimFail b


type Explanation = H String

--
-- DESIGN NOTE:
-- Genuine Writer style easier to comprehend than optimised
-- State style for explantions - often we want to censor 
-- Explanations and having them percolate inner-to-outer is 
-- easier to think about.
--

newtype CheckCode o a = CheckCode { 
    getCheckCode :: o -> (Explanation, a) }


instance Functor (CheckCode o) where
  fmap f ma = CheckCode $ \r -> let (w,a) = getCheckCode ma r in (w, f a)

instance Applicative (CheckCode o) where
  pure a    = CheckCode $ \_ -> (emptyH, a)
  mf <*> ma = CheckCode $ \r -> 
                let (w1,f) = getCheckCode mf r
                    (w2,a) = getCheckCode ma r
                in (w1 <> w2, f a)

instance Monad (CheckCode o) where
  return    = pure
  ma >>= k  = CheckCode $ \r -> 
                let (w1,a) = getCheckCode ma r 
                    (w2,b) = getCheckCode (k a) r
                in (w1 <> w2, b)



instance Monoid a => Monoid (CheckCode o a) where
  mempty = pure mempty
  ma `mappend` mb = CheckCode $ \r -> 
                      let (w1,a) = getCheckCode ma r
                          (w2,b) = getCheckCode mb r
                      in (w1 <> w2, a <> b) 
                               


answerOK :: (Explanation, Result)
answerOK = (emptyH, OK)

answerUserFail :: ErrorMessage ->  (Explanation, Result)
answerUserFail msg = (emptyH, UserFail msg)

answerPrimFail :: ErrorMessage ->  (Explanation, Result)
answerPrimFail msg = (emptyH, PrimFail msg)


-- | Build a polymorphic answer.
answerPoly :: a -> (Explanation, a)
answerPoly a = (emptyH, a)


-- Note - CheckCode cannot support Alternative / MonadPlus 
-- (no built-in notion of failure), similarly CheckFun cannot 
-- support Alternative / MonadPlus (not a functor).





runChecker :: Checker p o -> o -> Either (CheckError p) ()
runChecker spec@(Checker { checker_priority = p, checker_name = name }) r = 
    case getCheckCode (checker_code spec) r of
      (_,OK)          -> Right ()
      (w,UserFail s)  -> Left $ mkErr "%s - %s"     s w
      (w,PrimFail s)  -> Left $ mkErr "%s - ''%s''" s w
  where
    mkErr fmt s w = CheckError p (errMsg2 fmt name s) (unH w)


runCheckers :: [Checker p o] -> o -> [CheckError p]
runCheckers cs r = lefts $ map (runChecker `flip` r) cs


runGroup :: CheckerGroup p o -> o -> IssueGroup p
runGroup spec r = IssueGroup 
    { issue_group_name  = group_name spec
    , issues_found      = runCheckers (group_checker_specs spec) r 
    } 

runGroups :: GetName o => [CheckerGroup p o] -> o -> CheckReport p
runGroups gs r = CheckReport 
    { object_name       = getName r
    , issue_groups      = map (runGroup `flip` r) gs
    }


-- Should annotate have type:
--
-- > String -> CheckCode o a -> CheckCode o a
-- 
annotate :: String -> CheckCode o () 
annotate msg = CheckCode $ \_ -> (wrapH msg, ())


censor :: CheckCode o a -> CheckCode o a
censor ma = CheckCode $ \r -> 
    let (_,a) = getCheckCode ma r in (emptyH, a)

failure :: CheckFun o
failure = CheckCode $ \_ -> answerPrimFail "failure"



throwError  :: ErrorMessage -> CheckFun o
throwError msg = CheckCode $ \_ -> answerUserFail msg


        

substError :: ErrorMessage -> CheckFun o -> CheckFun o
substError msg p = CheckCode $ \r  -> 
    case getCheckCode p r of
        (_,OK)  -> answerOK
        (w1,_)  -> (w1, UserFail msg)
        

-- | Should only be used for building /combinators/.
swapPrimError :: CheckFun o -> ErrorMessage -> CheckFun o
swapPrimError p msg = CheckCode $ \r  -> 
    case getCheckCode p r of
        (w1,PrimFail _)  -> (w1, PrimFail msg)
        ans              -> ans


infixl 4 <??>

-- | infix version of @substError@
--
(<??>) :: CheckFun o -> ErrorMessage -> CheckFun o
(<??>) = flip substError


infixr 3 <&&> 
(<&&>) :: CheckFun o -> CheckFun o -> CheckFun o
(<&&>) = mappend


infixr 2 <||>

(<||>) :: CheckFun o -> CheckFun o -> CheckFun o
(<||>) = alt




-- TODO - is this the best way to combine errors?
--
alt :: CheckFun o -> CheckFun o -> CheckFun o
alt p q = CheckCode $ \r -> 
    case getCheckCode p r of
        (_,OK)          -> answerOK

        (w1,PrimFail _)  -> case getCheckCode q r of
            (_,OK)            -> answerOK
            (w2, UserFail e2) -> (w1 <> w2, UserFail e2)
            (w2, PrimFail _)  -> (w1 <> w2, PrimFail "alt")

        (w1,UserFail e1) -> case getCheckCode q r of
            (_,OK)            -> answerOK
            (w2, UserFail e2) -> (w1 <> w2, UserFail $ unwords [e1,e2])
            (w2, PrimFail _)  -> (w1 <> w2, UserFail e1)




-- aka Reader monad\'s local...
focus :: (o -> o1) -> CheckCode o1 a -> CheckCode o a
focus proj ma = CheckCode $ \u -> getCheckCode ma (proj u)



-- Note - a previous experiment turned focus into an operator 
-- giving us /paths/ - however precedence turned out badly.
-- Nicer syntax seems to be to actually use bracketed
-- reverse composition of selectors.

-- focus ( _parent >>> _child ) $ ...




-- | Can even have /self/ for oo fans.
--
self :: o -> o 
self = id

selftest :: (o -> Bool) -> (o -> ErrorMessage) -> CheckFun o
selftest test errk = CheckCode $ \r -> 
    if test r then answerOK else answerUserFail $ errk r

selftest_ :: (o -> Bool) -> CheckFun o
selftest_ test = CheckCode $ \r -> 
    if test r then answerOK else answerPrimFail "selftest"


assert :: Bool -> ErrorMessage -> Result
assert True  _   = OK
assert False msg = UserFail msg

genAssert_ :: Bool -> ErrorMessage -> Result
genAssert_ True  _    = OK
genAssert_ False msg  = PrimFail msg

assert_ :: Bool -> Result
assert_ = genAssert_ `flip` "assert_"


assert1 :: (a -> Bool) -> (a -> ErrorMessage) -> a -> Result
assert1 test errk a = assert (test a) (errk a)

assert1_ :: (a -> Bool) -> a -> Result
assert1_ test a = genAssert_  (test a) "assert1_"


assert2 :: (a -> b -> Bool) -> (a -> b -> ErrorMessage) -> a -> b -> Result
assert2 test errk a b = assert (test a b) (errk a b)

assert2_ :: (a -> b -> Bool) ->  a -> b -> Result
assert2_ test a b = genAssert_ (test a b) "assert2_"



ask :: CheckCode o o
ask = CheckCode $ \r -> answerPoly $ r

asks :: (o -> a) -> CheckCode o a
asks fn = CheckCode $ \r -> answerPoly $ fn r

-- | Possibly @get@ looks nicer than @asks@...
--
get :: (o -> a) -> CheckCode o a
get fn = CheckCode $ \r -> answerPoly $ fn r


--
-- We want an whenTrue combinator that checks onlyif True
-- but doesn\'t fail if False. E.g.:
--
-- > whenif (size>5) checkFullyUtilized  -- otherwise OK 
--
-- This is the reason for the special `ShortCircuitOkay`
-- constructor. 
--

whenTrue :: Bool -> CheckFun o -> CheckFun o
whenTrue True  ma = CheckCode $ \r -> getCheckCode ma r 
whenTrue False _  = CheckCode $ \_ -> answerOK 

unlessTrue :: Bool -> CheckFun o -> CheckFun o
unlessTrue True  _  = CheckCode $ \_ -> answerOK 
unlessTrue False ma = CheckCode $ \r -> getCheckCode ma r 


whenOK :: CheckFun o -> CheckFun o -> CheckFun o
whenOK mtest mb = CheckCode $ \r -> 
    case getCheckCode mtest r of
      (_,OK)  -> getCheckCode mb r
      _       -> answerOK

unlessOK :: CheckFun o -> CheckFun o -> CheckFun o
unlessOK mtest mb = CheckCode $ \r -> 
    case getCheckCode mtest r of
      (_,OK) -> answerOK
      _      -> getCheckCode mb r 


-- Note - a monadic version of onlyif would save some binding 
-- in user code, but is it sufficiently useful?
--
-- > onlyifM :: CheckCode o Bool -> CheckCode o a -> CheckCode o a
--




-- Note whenJust is a different sort of function to whenTrue and whenOK
--
whenJust :: CheckFun o -> CheckFun (Maybe o)
whenJust ma = CheckCode $ \r -> case r of
    Just r1 -> getCheckCode ma r1
    Nothing -> answerOK



onlyJust ::  CheckFun o -> CheckFun (Maybe o)
onlyJust ma = CheckCode $ \r -> case r of
    Just r1 -> getCheckCode ma r1
    Nothing -> answerPrimFail "onlyJust"


-- | Patterning the functions onlyLeft and onlyRight on onlyJust
-- makes sense...
--
whenLeft :: CheckFun o -> CheckFun (Either o o1)
whenLeft ma = CheckCode $ \r -> case r of
    Left r1 -> getCheckCode ma r1
    _       -> answerOK


whenRight :: CheckFun o -> CheckFun (Either o0 o)
whenRight ma = CheckCode $ \r -> case r of
    Right r1 -> getCheckCode ma r1
    _        -> answerOK



onlyLeft :: CheckFun o -> CheckFun (Either o o1)
onlyLeft ma = CheckCode $ \r -> case r of
    Left r1 -> getCheckCode ma r1
    _       -> answerPrimFail "onlyLeft"


onlyRight :: CheckFun o -> CheckFun (Either o0 o) 
onlyRight ma = CheckCode $ \r -> case r of
    Right r1 -> getCheckCode ma r1 
    _        -> answerPrimFail "onlyRight"


checkall :: F.Foldable t => CheckFun u  -> CheckFun (t u)
checkall ma = CheckCode $ \r -> 
    F.foldr (\e ac -> ac `comb` getCheckCode ma e) (emptyH,OK) r 
  where
    (_,OK) `comb` (_,OK) = answerOK
    (_,OK) `comb` accb   = accb
    acca   `comb` (_,OK) = acca
    (w1,a) `comb` (w2,b) = (w1 <> w2, a <> b)



checkany :: F.Foldable t => CheckFun u  -> CheckFun (t u)
checkany ma = CheckCode $ \r -> 
    F.foldr (\e ac -> ac `comb` getCheckCode ma e) (emptyH, PrimFail "checkany") r
  where
    (_,OK) `comb` _       = answerOK 
    _      `comb` (_,OK)  = answerOK
    (w1,a) `comb` (w2,_)  = (w1 <> w2,a)



checkfirst :: F.Foldable t => CheckFun u  -> CheckFun (t u)
checkfirst ma = CheckCode $ \r -> 
    getCheckCode (chkfirst ma `swapPrimError` "checkfirst") (F.toList r)

chkfirst :: CheckFun u  -> CheckFun [u]
chkfirst ma = CheckCode $ \r -> case r of
    (x:_) -> getCheckCode ma x
    []    -> answerPrimFail "chkfirst"


checklast :: F.Foldable t => CheckFun u  -> CheckFun (t u)
checklast ma = CheckCode $ \r -> 
    getCheckCode (chklast ma `swapPrimError` "checklast") (F.toList r)

chklast :: CheckFun u  -> CheckFun [u]
chklast ma = CheckCode $ \r -> step r
  where
    step []     = answerPrimFail "chklast"
    step [x]    = getCheckCode ma x
    step (_:xs) = step xs 


--------------------------------------------------------------------------------
-- Indexed Access



indexed :: Indexed t => Int -> CheckFun u -> CheckFun (t u)
indexed i ma = CheckCode $ \r -> case ixlookup i r of
    Just a  -> getCheckCode ma a
    Nothing -> answerPrimFail "indexed"



class Indexed (t :: * -> *) where
  ixlookup :: Int -> t a -> Maybe a

instance Indexed IM.IntMap where
  ixlookup = IM.lookup


instance Indexed [] where
  ixlookup i xs = case splitAt i xs of
                    (_,(x:_)) -> Just x
                    (_,[])    -> Nothing
  


newtype ZeroIxList a = ZeroIxList { getZeroIxList :: [a] } 
  deriving (Eq,Ord,Read,Show)

newtype OneIxList a = OneIxList { getOneIxList :: [a] } 
  deriving (Eq,Ord,Read,Show)


zeroIndexedList :: [a] -> ZeroIxList a
zeroIndexedList = ZeroIxList

oneIndexedList :: [a] -> OneIxList a
oneIndexedList = OneIxList


instance Indexed ZeroIxList where
  ixlookup i = ixlookup i . getZeroIxList

instance Indexed OneIxList where
  ixlookup i xs = case splitAt (i-1) $ getOneIxList xs of
                    (_,(x:_)) -> Just x
                    (_,[])    -> Nothing




--------------------------------------------------------------------------------
-- Counting checks


-- | TODO - look at better explanation...
--
countingChecker :: F.Foldable t 
                => (Int -> Bool) -> CheckFun u  -> CheckFun (t u)
countingChecker test ma = CheckCode $ \r -> 
    let (w1,ans1) = F.foldr (\e ac -> ac `comb` getCheckCode ma e) (emptyH,0) r
    in if test ans1 then answerOK 
                    else (w1, PrimFail $ "countingChecker " ++ show ans1)
  where
    (w1,n) `comb` (_ ,OK) = (w1, n + 1)
    (w1,n) `comb` (w2,_)  = (w1 <> w2, n)


exactly :: F.Foldable t => Int -> CheckFun u  -> CheckFun (t u)
exactly n ma = countingChecker (== n) ma <??> "exactly"

atmost :: F.Foldable t => Int -> CheckFun u  -> CheckFun (t u)
atmost n ma = countingChecker (<= n) ma <??> "atmost"

atleast :: F.Foldable t => Int -> CheckFun u  -> CheckFun (t u)
atleast n ma = countingChecker (>= n) ma <??> "atleast"

withinCount :: F.Foldable t => (Int,Int) -> CheckFun u  -> CheckFun (t u)
withinCount (mmin,mmax) ma = 
    countingChecker (\i -> i >= mmin && i <= mmax) ma <??> "withinCount"



--------------------------------------------------------------------------------
-- Error messages

-- Printf string interpolation is very convenient for error messages...

errMsg0 :: String -> ErrorMessage
errMsg0 = id


errMsg1 :: PrintfArg a => String -> a -> ErrorMessage
errMsg1 fmt a = printf fmt a


errMsg2 :: (PrintfArg a, PrintfArg b) => String -> a -> b -> ErrorMessage
errMsg2 fmt a b = printf fmt a b


errMsg3 :: (PrintfArg a, PrintfArg b, PrintfArg c) 
        => String -> a -> b -> c -> ErrorMessage
errMsg3 fmt a b c = printf fmt a b c


errMsg4 :: (PrintfArg a, PrintfArg b, PrintfArg c, PrintfArg d) 
        => String -> a -> b -> c -> d -> ErrorMessage
errMsg4 fmt a b c d = printf fmt a b c d


errMsg5 :: (PrintfArg a, PrintfArg b, PrintfArg c, PrintfArg d, PrintfArg e) 
        => String -> a -> b -> c -> d -> e -> ErrorMessage
errMsg5 fmt a b c d e = printf fmt a b c d e


--------------------------------------------------------------------------------
-- Report

class GetName obj where
  getName :: obj -> String

class Priority p where
  priorityName :: p -> String


data CheckReport p = CheckReport 
    { object_name       :: String
    , issue_groups      :: [IssueGroup p]
    }
  deriving Show


data IssueGroup p = IssueGroup
    { issue_group_name  :: String
    , issues_found      :: [CheckError p]
    } 
  deriving Show


blank :: Doc
blank = text ""

underline :: String -> Doc
underline s = let n = length s in text s $+$ text (replicate n '-')


printReportSimple :: Priority p => CheckReport p -> String
printReportSimple r = render $ body $+$ blank
  where 
    body    = F.foldl' ($+$) title issues
    title   = underline $ object_name r
    issues  = catMaybes $ map ppIssueGroup $ issue_groups r

ppIssueGroup  :: Priority p => IssueGroup p -> Maybe Doc
ppIssueGroup (IssueGroup _ []) = Nothing
ppIssueGroup (IssueGroup s xs) = Just body
  where
    body  = F.foldl' ($+$) title $ map ppErr xs
    title = text "Checker Group -" <+> text s

ppErr :: Priority p => CheckError p -> Doc
ppErr (CheckError p msg w)
    | null w    = body
    | otherwise = body $+$ nest 2 (vcat $ map text w)
  where
    body = text (priorityName p) P.<> text ":" <+> text msg

